open import Ideal using (Ideal ; IsIdeal ; R/I-isRing)
open import II-1-1 using (th1-1)
open import Algebra using (Ring ; AbelianGroup; Group ; Monoid)
open import Algebra.Structures using ()
open import Substructures using ( IsSubGroup ; IsNormalSubGroup; everySubGroupOfAbelianIsNormal )
open import Kern using ()
open import Level using (Level ; _⊔_ )
open import Relation.Unary using (Pred ; _∈_)
open import Algebra.Morphism using (IsGroupMorphism ; IsRingMorphism ; IsAbelianGroupMorphism ; IsSemigroupMorphism ; IsMonoidMorphism)
open import Function
import Relation.Binary.EqReasoning as EqR

module II-2-1 where
{--
The fundamental theorem of homomorphisms of rings follows immediately
from the corresponding theorem for groups


2.1 THEOREM
Let I be an ideal in the ring R. 

If f is a homomorphism from R to a ring S with f(I) = 0
then f is a homomorphism from  R/I to S.
 If fmaps onto S and the kernel of f is I then 
 f is an imsomorphism from R/I to S.
--}


module _  {cᵣ ℓᵣ cₛ ℓₛ : Level }  (R : Ring  cᵣ ℓᵣ) (S : Ring cₛ ℓₛ) where
  open Ring R renaming ( Carrier to Carrierᵣ ; _≈_ to _≈ᵣ_ ; _+_ to _+ᵣ_
                       ; _*_ to _∙ᵣ_ ; -_ to -ᵣ_ ; 0# to 0ᵣ ; 1# to 1ᵣ
                       ; isRing to isRingᵣ ; +-abelianGroup to +-abelianGroupᵣ
                       ; +-group to +-groupᵣ ; *-monoid to ∙-monoidᵣ
                       ; +-assoc to +-assocᵣ ; *-cong to ∙-congᵣ
                       ; *-assoc to ∙-assocᵣ ; sym to symᵣ ; setoid to setoidᵣ
                       ; refl to reflᵣ)
  open Ring S renaming ( Carrier to Carrierₛ ; _≈_ to _≈ₛ_ ; _+_ to _+ₛ_
                       ; _*_ to _∙ₛ_ ; -_ to -ₛ_ ; 0# to 0ₛ ; 1# to 1ₛ
                       ; isRing to isRingₛ; +-abelianGroup to +-abelianGroupₛ
                       ; +-group to +-groupₛ ; *-monoid to ∙-monoidₛ 
                       ; setoid to setoidₛ ; sym to symₛ ; refl to reflₛ)
  module _ {p : Level} {f : Carrierᵣ → Carrierₛ} {Iₚ : Pred Carrierᵣ p}
           (isIdeal : IsIdeal Iₚ _≈ᵣ_ _+ᵣ_ _∙ᵣ_ -ᵣ_ 0ᵣ 1ᵣ) (isRingMorphism : IsRingMorphism R S f)
           where
    open IsRingMorphism isRingMorphism
    I : Ideal cᵣ p ℓᵣ
    I = record { isIdeal = isIdeal }
    open IsIdeal isIdeal

    R/I : Ring cᵣ p
    R/I = record { isRing = R/I-isRing I }

    open Ring R/I renaming ( Carrier to Carrierᵢ ; _≈_ to _≈ᵢ_ ; _+_ to _+ᵢ_
                           ; _*_ to _∙ᵢ_ ; -_ to -ᵢ_ ; 0# to 0ᵢ ; 1# to 1ᵢ
                           ; isRing to isRingᵢ ; +-abelianGroup to +-abelianGroupᵢ
                           ; +-group to +-groupᵢ ; *-monoid to ∙-monoidᵢ) 

    module _ (fₚ : (x : Carrierᵣ) → (_ : x ∈ Iₚ) → ((f x) ≈ₛ 0ₛ)) where
      tw-II-2-1-I : IsRingMorphism R/I S f
      Algebra.Morphism.IsAbelianGroupMorphism.gp-homo (IsRingMorphism.+-abgp-homo tw-II-2-1-I) = let
          thisShouldBeSufficient : IsGroupMorphism _ +-groupₛ f
          thisShouldBeSufficient = th1-1 +-groupᵣ +-groupₛ Iₚ
            (everySubGroupOfAbelianIsNormal +-abelianGroupᵣ Iₚ isSubGroup)
            f fₚ (IsAbelianGroupMorphism.gp-homo +-abgp-homo)
          -- Agda nie może znunifikować R.group z I.group więc to powyżej nie wystarczy (zauważ '_'). Trzeba kombinować
          flol : Carrierᵢ → Carrierₛ
          flol = f
          +ria = Ring.+-abelianGroup $ Ideal.ring I
          +ri : Group _ _
          +ri = AbelianGroup.group $ +ria
          q : (f 0ᵣ) ≈ₛ 0ₛ
          q = IsAbelianGroupMorphism.ε-homo (IsRingMorphism.+-abgp-homo isRingMorphism)
          cngQ : {a b : Carrierᵢ}  → a ≈ᵣ b →  (f a) ≈ₛ (f b)
          cngQ p = IsAbelianGroupMorphism.⟦⟧-cong  (IsRingMorphism.+-abgp-homo isRingMorphism) p
          hq : (a b : Carrierᵣ) → (f (a +ᵣ b)) ≈ₛ (f a) +ₛ (f b)
          hq = IsAbelianGroupMorphism.∙-homo (IsRingMorphism.+-abgp-homo isRingMorphism) 
          iSm :  IsSemigroupMorphism _ _ f
          iSm = record { ⟦⟧-cong = λ {a} {b} a≈b → cngQ a≈b  ; ∙-homo = hq }
          iGm : IsGroupMorphism +ri +-groupₛ flol
          iGm = record { mn-homo = record { ε-homo = q ; sm-homo = iSm }}
          thisShouldBeSufficientQ : IsGroupMorphism +-groupᵢ +-groupₛ flol
          thisShouldBeSufficientQ = th1-1 +ri +-groupₛ Iₚ ((everySubGroupOfAbelianIsNormal +ria Iₚ isSubGroup))
           flol fₚ iGm
          -- CAŁY TEN BAŁAGAN OD POPRZEDNIEGO KOMENTZRZA TO TYLKO PRZEZ BRAK UNIFIKACJI XDDDD
          thisShouldBeSufficient' : IsGroupMorphism +-groupᵢ +-groupₛ f
          thisShouldBeSufficient' = thisShouldBeSufficientQ 
        in thisShouldBeSufficient'
      IsRingMorphism.*-mn-homo tw-II-2-1-I = let -- to też nie powinno być tak skomplikowane
          mph = IsRingMorphism.*-mn-homo isRingMorphism
          eh : f 1ᵣ ≈ₛ 1ₛ
          eh = IsMonoidMorphism.ε-homo mph
          hq : (a b : Carrierᵣ) → (f (a ∙ᵣ b)) ≈ₛ (f a) ∙ₛ (f b)
          hq = IsMonoidMorphism.∙-homo mph
--          R/I
          mcong = IsMonoidMorphism.⟦⟧-cong  mph
          mhomo = IsMonoidMorphism.∙-homo  mph
--          h1 : {a b : Carrierᵣ} → a ≈ᵣ a
          h1 : {a b : Carrierᵣ} → a ≈ᵣ ((a +ᵣ (-ᵣ b)) +ᵣ b)
          h1 {a} {b} = let open EqR setoidᵣ in begin
            a ≈⟨  symᵣ $ Group.identityʳ  +-groupᵣ a ⟩
            a +ᵣ 0ᵣ ≈⟨ Group.∙-cong +-groupᵣ reflᵣ (symᵣ $ Group.inverseˡ +-groupᵣ b) ⟩
            a +ᵣ ((-ᵣ b) +ᵣ b) ≈⟨ symᵣ $ Group.assoc +-groupᵣ _ _ _ ⟩ 
            (a +ᵣ (-ᵣ b)) +ᵣ b ∎
--          h1 b = (symᵣ $ Group.inverseʳ +-groupᵣ b)
          cngQ : {a b : Carrierᵢ}  → a +ᵣ (-ᵣ b) ∈ Iₚ →  (f a) ≈ₛ (f b)
          cngQ {a} {b} a≈ᵢb = let open EqR setoidₛ in begin
            f a ≈⟨ mcong h1 ⟩
            f ((a +ᵣ (-ᵣ b)) +ᵣ b) ≈⟨ IsAbelianGroupMorphism.∙-homo  (IsRingMorphism.+-abgp-homo isRingMorphism) _ _  ⟩
            (f (a +ᵣ (-ᵣ b))) +ₛ (f b) ≈⟨  Group.∙-cong +-groupₛ (fₚ _ a≈ᵢb )  reflₛ   ⟩
            0ₛ +ₛ (f b) ≈⟨  Group.identityˡ +-groupₛ (f b) ⟩
            f b ∎
          iSm : IsSemigroupMorphism (Monoid.semigroup ∙-monoidᵢ) (Monoid.semigroup ∙-monoidₛ) f
          iSm = record {⟦⟧-cong = cngQ ; ∙-homo = hq} 
        in record {sm-homo = iSm ; ε-homo = eh}
